Termination Proof Script

• Consider the SCC {44,58}. There are no usable rules. By taking the AF π with π(CONS) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 44 is weakly decreasing and rule 58 is strictly decreasing. There is one new SCC.
  • Consider the SCC {44}. By taking the AF π with π(CONS) = 1 together with the lexicographic path order with empty precedence, rule 44 is strictly decreasing.


• Consider the SCC {41,42,56}. There are no usable rules. By taking the AF π with π(FIRST) = π(mark) = 1 together with the lexicographic path order with empty precedence, the rules in {41,42} are weakly decreasing and rule 56 is strictly decreasing. There is one new SCC.
  • Consider the SCC {41,42}. By taking the AF π with π(FIRST) = 1 together with the lexicographic path order with empty precedence, rule 42 is weakly decreasing and rule 41 is strictly decreasing. There is one new SCC.
    • Consider the SCC {42}. By taking the AF π with π(FIRST) = 2 together with the lexicographic path order with empty precedence, rule 42 is strictly decreasing.


• Consider the SCC {45,59}. There are no usable rules. By taking the AF π with π(FROM) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 45 is weakly decreasing and rule 59 is strictly decreasing. There is one new SCC.
  • Consider the SCC {45}. By taking the AF π with π(FROM) = 1 together with the lexicographic path order with empty precedence, rule 45 is strictly decreasing.


• Consider the SCC {43,57}. There are no usable rules. By taking the AF π with π(mark) = π(S) = 1 together with the lexicographic path order with empty precedence, rule 43 is weakly decreasing and rule 57 is strictly decreasing. There is one new SCC.
  • Consider the SCC {43}. By taking the AF π with π(S) = 1 together with the lexicographic path order with empty precedence, rule 43 is strictly decreasing.


• Consider the SCC {47,48,50,52,53,55}. There are no usable rules. By taking the AF π with π(from) = π(PROPER) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {50,55} are weakly decreasing and the rules in {47,48,52,53} are strictly decreasing. There is one new SCC.
  • Consider the SCC {50,55}. By taking the AF π with π(from) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 55 is weakly decreasing and rule 50 is strictly decreasing. There is one new SCC.
    • Consider the SCC {55}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 55 is strictly decreasing.


• Consider the SCC {32,34,36,38,40}. There are no usable rules. By taking the AF π with π(ACTIVE) = π(cons) = π(from) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {36,38,40} are weakly decreasing and the rules in {32,34} are strictly decreasing. There is one new SCC.
  • Consider the SCC {36,38,40}. By taking the AF π with π(ACTIVE) = π(cons) = π(from) = 1 together with the lexicographic path order with empty precedence, the rules in {38,40} are weakly decreasing and rule 36 is strictly decreasing. There is one new SCC.
    • Consider the SCC {38,40}. By taking the AF π with π(ACTIVE) = π(cons) = 1 together with the lexicographic path order with empty precedence, rule 38 is weakly decreasing and rule 40 is strictly decreasing. There is one new SCC.
      • Consider the SCC {38}. By taking the AF π with π(ACTIVE) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 38 is strictly decreasing.


• Consider the SCC {60,62}. The usable rules are {1-23}. By taking the AF π with π(active) = π(cons) = π(ok) = π(proper) = π(s) = π(TOP) = 1 together with the lexicographic path order with precedence 0 ≻ mark, 0 ≻ nil, first ≻ mark and from ≻ mark, the rules in {4-8,11,12,14-23,62} are weakly decreasing and the rules in {1-3,9,10,13,60} are strictly decreasing. There is one new SCC.
  • Consider the SCC {62}. The usable rules are {1-13,20-23}. By taking the AF π with π(active) = π(first) = π(from) = π(mark) = π(s) = π(TOP) = 1 and π(cons) = 2 together with the lexicographic path order with precedence 0 ≻ nil, the rules in {2-13,20-23} are weakly decreasing and the rules in {1,62} are strictly decreasing.